theory SemReach imports Main ClangSem ClangEv
begin

(* note: does not track Cseq labels *)
--"stmcl s1 s2 = statement s2 is (possibly) reachable from statement s1"
fun clwh:: "'l option \<Rightarrow> 'm bexpr \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> bool" 
and clseq :: "'l option \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> bool"
and stmcl :: "('pn,'m,'n,'l) stmt \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> bool"
where
  "clwh lb be s (Cseq lb' s1' s2') = (stmcl s s1' \<and> s2' = (Cwhile lb be s))"
| "clwh lb be s s' = (s' = (Cwhile lb be s) \<or> s' = (Cnone lb))"

(*| "clseq lb (Cnone lb1) s s' = (stmcl s s')"*)
| "clseq lb s1 s2 (Cseq lb' s1' s2') = (((stmcl s1 s1') \<and> s2 = s2') \<or> (stmcl s2 (Cseq lb' s1' s2')))"
| "clseq lb s1 s2 s' = (stmcl s2 s')"

| "stmcl (Cnone lb) s' = (s' = (Cnone lb))"
| "stmcl (Cseq lb s1 s2) s' = (s' = (Cseq lb s1 s2) \<or> clseq lb s1 s2 s')"
| "stmcl (Casg lb x e) s' = (s' = (Casg lb x e) \<or> s' = (Cnone lb))"
| "stmcl (Cif lb be s1 s2) s' = (s' = (Cif lb be s1 s2) \<or> stmcl s1 s' \<or> stmcl s2 s')"
| "stmcl (Cwhile lb be s) s' = (s' = (Cwhile lb be s) \<or> clwh lb be s s')"
| "stmcl (Cread lb x y) s' = (s' = (Cread lb x y) \<or> s' = (Cnone lb))"
| "stmcl (Cwrite lb x y) s' = (s' = (Cwrite lb x y) \<or> s' = (Cnone lb))"
| "stmcl (Cwait lb wcs s) s' = (s' = (Cwait lb wcs s) \<or> stmcl s s')"

lemma stmcl_fix: "stmcl s s" by (cases s, simp_all)
lemma clseq_fix: "clseq lb s1 s2 s2" by (cases s2, simp_all)
lemma lem_clseq_ex: "clseq lb s1 s2 s' = (stmcl s2 s' \<or> (\<exists> lb' s1' . stmcl s1 s1' \<and> s' = (Cseq lb' s1' s2)))"
  by (cases s', auto)

lemma lem_stmcl_he1:
  assumes a0: "s = (Cseq lb s1 s2)"
  and a1:"\<forall> s1' . transition s1 q io s1' q' \<longrightarrow> stmcl s1 s1'"
  and a2: "transition s q io s' q'"
  shows "stmcl s s'"
using a0 a2
apply(cases s, simp_all)
apply(case_tac "\<exists> x . stmt1 = Cnone x", simp_all add: stmcl_fix) (*1 goal*)
apply(clarify)
apply(simp add: stmcl_fix)
apply(simp add: clseq_fix)
proof - (* s' is Cseq *)
  fix lbx s1x s2x
  assume c0: "lbx = lb \<and> s1x = s1 \<and> s2x = s2"
  assume c1: "s = Cseq lb s1 s2"
  assume c2:"case s1 of Cnone x \<Rightarrow> s' = s2 \<and> io = ANone \<and> q' = q | _ \<Rightarrow> (case s' of Cseq None s1' s2' \<Rightarrow> s2' = s2 \<and> transition s1 q io s1' q' | Cseq (Some a) s1' s2' \<Rightarrow> False | _ \<Rightarrow> False)" "\<forall>x. s1 \<noteq> Cnone x"
  then have "case s' of Cseq None s1' s2' \<Rightarrow> s2' = s2 \<and> transition s1 q io s1' q' | Cseq (Some a) s1' s2' \<Rightarrow> False | _ \<Rightarrow> False"
    by (cases s1, simp_all)
  from this c1 show "s' = (Cseq lb s1 s2) \<or> clseq lb s1 s2 s'"
    apply(cases s', simp_all)
    apply(case_tac "option", simp_all)
    proof -
      fix option stmt1 stmt2
      assume "stmt2 = s2 \<and> transition s1 q io stmt1 q'" "s' = Cseq None stmt1 s2" "s = Cseq lb s1 s2" "option = None"
      moreover then have "stmcl s1 stmt1" using a1 by blast
      ultimately show "None = lb \<and> stmt1 = s1 \<or> stmcl s1 stmt1 \<or> stmcl s2 (Cseq None stmt1 s2)"
        (*"None = lb \<and> stmt1 = s1 \<or> clseq lb s1 s2 (Cseq None stmt1 s2)"*)
        by (cases s1, simp_all)
    qed
(*next only if we skip Cnone case in clseq and skip io = ANone and q' = q
  fix x
  assume "s' = s2" "\<not> clseq lb (Cnone x) s2 s2"
  then show "s2 = Cseq lb (Cnone x) s2" using clseq_fix by blast*)
qed

lemma lem_stmcl_he2: "\<forall> s' . transition s q io s' q' \<longrightarrow> stmcl s s'"
apply(induct s)
apply(simp)                      --"Cnone"
apply(metis lem_stmcl_he1)       --"Cseq"
apply(case_tac "expr", simp_all) --"Casg, Cread, Cwrite"
apply(case_tac "eval_bexpr q bexpr", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)
apply(simp add: stmcl_fix)
apply(simp add: stmcl_fix)       --"Cif"
apply(case_tac "eval_bexpr q bexpr", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)
apply(clarify)
apply(case_tac "s'", simp_all)
apply(simp add: stmcl_fix)       --"Cwhile"
apply(simp add: stmcl_fix)       --"Cwait"
done

lemma lem_stmcl: "transition s q io s' q' \<Longrightarrow> stmcl s s'" --"soundness"
  using lem_stmcl_he2 by blast

lemma lem_seq_he: "stmcl s s' \<Longrightarrow> clseq lb s0 s s'"
apply(cases s0, auto)
apply(cases s', simp_all)
apply(cases s', simp_all)
apply(cases s', simp_all)
apply(cases s', simp_all)
apply(cases s', simp_all)
apply(cases s', simp_all)
apply(cases s', simp_all)
apply(cases s', simp_all) (* only if we skip Cnone case in clseq *)
done

lemma stmcl_trans_he: "\<forall> s2 s3 . stmcl s1 s2 \<and> stmcl s2 s3 \<longrightarrow> stmcl s1 s3"
apply(induct s1)
apply(auto)
proof -
  fix lb s11 s12 s2 s3
  assume a2:"stmcl s2 s3" "clseq lb s11 s12 s2"
  assume a3: "\<not> clseq lb s11 s12 s3"
  assume a0:"\<forall>s2 s3. stmcl s11 s2 \<and> stmcl s2 s3 \<longrightarrow> stmcl s11 s3"
  assume a1:"\<forall>s2 s3. stmcl s12 s2 \<and> stmcl s2 s3 \<longrightarrow> stmcl s12 s3"
  {
    assume "\<exists> lb' s1'. stmcl s11 s1' \<and> s2 = Cseq lb' s1' s12"
    then obtain lb' s1' where c1:"stmcl s11 s1' \<and> s2 = Cseq lb' s1' s12" by blast
    from this a2 have "s3 = s2 \<or> clseq lb' s1' s12 s3" by auto
    moreover {
      assume "s3 = s2"
      from this a2 have "clseq lb s11 s12 s3" by simp
    }
    moreover {
      assume "clseq lb' s1' s12 s3"
      then have "(stmcl s12 s3 \<or> (\<exists> lbx s1x . stmcl s1' s1x \<and> s3 = (Cseq lbx s1x s12)))" using lem_clseq_ex by blast
      moreover {
        assume "\<exists> lbx s1x . stmcl s1' s1x \<and> s3 = (Cseq lbx s1x s12)"
        then obtain lbx s1x where "stmcl s1' s1x \<and> s3 = (Cseq lbx s1x s12)" by blast
        moreover from this c1 a0 have "stmcl s11 s1x" by blast
        ultimately have "(\<exists> lbx s1x. stmcl s11 s1x \<and> s3 = Cseq lbx s1x s12)" by blast
      }
      ultimately have "clseq lb s11 s12 s3" using a2 a1 lem_clseq_ex by blast
    }
    ultimately have "clseq lb s11 s12 s3" by blast
  }
  from this a1 a2 a3 show "s3 = Cseq lb s11 s12" using lem_clseq_ex by blast
next
  fix lb be s1 s2 s3
  assume a2: "stmcl s2 s3" "clwh lb be s1 s2"
  assume a3:"\<not> clwh lb be s1 s3"
  assume a0:"\<forall> s2 s3. stmcl s1 s2 \<and> stmcl s2 s3 \<longrightarrow> stmcl s1 s3"
  from a2 have "clwh lb be s1 s3"
    apply(cases s2, auto)
    apply(cases s3, auto)
    apply(insert a0, blast)
    done
  from this a3 show "s3 = Cwhile lb be s1" by blast
qed

lemma stmcl_trans: "stmcl s1 s2 \<Longrightarrow> stmcl s2 s3 \<Longrightarrow> stmcl s1 s3" --"transitivity"
  using stmcl_trans_he by blast

(*----------------------------------------------------------------------*)


lemma lem_etrans_stmcl: "etrans (Some es) (Some es') \<Longrightarrow> stmcl (es_stm es) (es_stm es')"
apply(cases es, cases es', auto)
apply(case_tac "bool", auto simp add: stmcl_fix lem_stmcl)
done

lemma lem_exseq_stmcl_he0:
  assumes a0: "valid_gtrace tr"
  and a1:"exseq tr p i = Some es" "exseq tr p (Suc i) = Some es'"
  shows "stmcl (es_stm es) (es_stm es')"
using a0 a1 exseq_trans lem_etrans_stmcl by metis

lemma lem_exseq_stmcl_he1:
  assumes a0: "valid_gtrace tr" "exseq tr p 0 = Some es"
  shows "\<forall> es' . exseq tr p i = Some es' \<longrightarrow> stmcl (es_stm es) (es_stm es')"
apply(induct i)
apply(metis a0(2) stmcl_fix the.simps)
apply(clarify)
proof -
  fix i es'
  assume c0:"\<forall>es'. exseq tr p i = Some es' \<longrightarrow> stmcl (es_stm es) (es_stm es')"
  assume c1:"exseq tr p (Suc i) = Some es'"
  from this a0(1) obtain es1 where c2:"exseq tr p i = Some es1" using exseq_pre3 by metis
  from this a0(1) c1 have "stmcl (es_stm es1) (es_stm es')" using lem_exseq_stmcl_he0 by simp
  moreover from c0 c2 have "stmcl (es_stm es) (es_stm es1)" by blast
  ultimately show "stmcl (es_stm es) (es_stm es')" using stmcl_trans by blast
qed

lemma lem_exseq_stmcl_he2:
  assumes a0: "valid_gtrace tr"
  shows "\<forall> i es' . (exseq tr p i = Some es \<and> i \<le> j \<and> exseq tr p j = Some es' \<longrightarrow> stmcl (es_stm es) (es_stm es'))"
apply(induct j)
apply(clarify)
apply(metis a0 lem_exseq_stmcl_he1) --"case i=0"
proof (clarify)
  fix j i es'
  assume c0:"\<forall>i es'. exseq tr p i = Some es \<and> i \<preceq> j \<and> exseq tr p j = Some es' \<longrightarrow> stmcl (es_stm es) (es_stm es')"
  assume c1:"exseq tr p i = Some es" "i \<preceq> Suc j" "exseq tr p (Suc j) = Some es'"
  then have "i \<le> j \<or> i = Suc j" by auto
  moreover {
    assume d0:"i \<le> j"
    from a0 c1(3) obtain es1 where d1:"exseq tr p j = Some es1" using exseq_pre3 by metis
    from a0 this c1(3) have "stmcl (es_stm es1) (es_stm es')" using lem_exseq_stmcl_he0 by simp
    moreover from c1(1) c0 d0 d1 have "stmcl (es_stm es) (es_stm es1)" by blast
    ultimately have "stmcl (es_stm es) (es_stm es')" using stmcl_trans by blast
  }
  moreover {
    assume d0:"i = Suc j"
    from this c1 have "es = es'" by simp
    then have "stmcl (es_stm es) (es_stm es')" using stmcl_fix by blast
  }
  ultimately show "stmcl (es_stm es) (es_stm es')" by blast
qed

lemma lem_exseq_stmcl:
  assumes a0: "valid_gtrace tr" "i \<le> j" "exseq tr p i = Some es" "exseq tr p j = Some es'"
  shows "stmcl (es_stm es) (es_stm es')"
using a0 lem_exseq_stmcl_he2 by metis

lemma lem_ev_stmcl:
  assumes a0: "valid_gtrace tr" "globev tr e1" "globev tr e2"
  and a1: "e1 \<preceq> e2" "ge_proc e1 = ge_proc e2"
  shows "stmcl (ev_stm e1) (ev_stm e2)"
proof -
  from a1 obtain p where c1: "ge_proc e1 = p \<and> ge_proc e2 = p" by blast
  obtain i j where c2: "i = ge_n e1 \<and> j = ge_n e2" by blast
  from a0 c1 c2 have "exseq tr p i = Some (es_of_ev e1)" using ev_in_exseq by metis
  moreover from a0 c1 c2 have "exseq tr p j = Some (es_of_ev e2)" using ev_in_exseq by metis
  moreover from a1(1) c2 have "i \<le> j" using less_eq_gevent_def by blast
  ultimately have "stmcl (es_stm (es_of_ev e1)) (es_stm (es_of_ev e2))" using a0 lem_exseq_stmcl by metis
  then show ?thesis by simp
qed

lemma lem_init_stmcl:
  assumes a0: "prog_semantics pg tr"
  and a1:"globev tr e" "proc \<in> set pg" "proc_name proc = ge_proc e"
  shows "stmcl (proc_stm proc) (ev_stm e)"
proof -
  from a0 a1 obtain io bv where c0:"exseq tr (ge_proc e) 0 = Some (Estate (proc_stm proc) empty io bv)" using exseq_init by blast
  from a1 obtain p where c1:"proc_name proc = p \<and> ge_proc e = p" by blast
  obtain i where c2:"ge_n e = i" by blast
  from a0 have c3:"valid_gtrace tr" using prog_semantics_def by blast

  obtain es where d0:"es = (Estate (proc_stm proc) empty io bv)" by blast
  from c3 c2 c1 a1(1) have d1:"exseq tr p i = Some (es_of_ev e)" using ev_in_exseq by metis
  from d0 c0 c1 have d2:"exseq tr p 0 = Some es" by simp
  have "0 \<le> i" by auto
  from this d1 d2 c3 have "stmcl (es_stm es) (es_stm (es_of_ev e))" using lem_exseq_stmcl by metis
  from d0 this show ?thesis by simp
qed

end

(*
lemma lem_stm_pre:
  assumes a0: "prog_semantics pg tr"
  and a1:"globev tr e" "proc \<in> set pg" "proc_name proc = ge_proc e"
  shows "(ev_stm e = proc_stm proc) \<or> (\<exists> e' . e' \<prec> e \<and> globev tr e' \<and> ge_proc e' = ge_proc e)"
proof -
  {
    assume "ev_stm e \<noteq> proc_stm proc"
    
  }
qed
*)
